package ai.wprolog.essentials;

import java.util.Stack;

import util.essential.SourceGetter;

//Var is a type of Term.
/**
 * A Term is the basic data structure in Prolog. There are three types of terms:
 * <ol>
 * <li>Values (ie. have a functor and arguments)
 * <li>Variables (ie. unbound)
 * <li>References (bound to another variable)
 * </ol>
 */
public class Term {
	private String functor;
	private int arity;
	private Term args[];
	private static int varnum = 1;
	// If bound is false then term is a free variable
	private boolean bound;
	private int varid;
	// If bound is true and deref is true then the term is
	// a reference to ``ref''
	private boolean deref;
	private Term ref;

	/**
	 * Controls whether occurcheck is used in unification. Note that in version
	 * 1.0 the occurcheck was always performed which accounted for the lower
	 * performance.
	 */
	static public boolean occurcheck = false;

	/**
	 * prettyprint controls printing of lists as <tt>[a,b]</tt> rather than
	 * <tt>cons(a,cons(b,null))</tt>
	 */
	static public boolean prettyprint = true;

	/**
	 * Controls whether predicates can begin with an underscore. Beginning a
	 * system with an underscore makes in inaccessible to the user.
	 */
	static public boolean internalparse = false;

	/** create fresh var */
	public Term() {
		varid = varnum++;
		bound = false;
		deref = false;
	}

	/** create var with specified varid */
	public Term(int i) {
		varid = i;
		bound = false;
		deref = false;
	}

	/**
	 * create a term with a given functor and arity.
	 * 
	 * @param s
	 *            - the functor
	 * @param a
	 *            - the arity
	 */
	public Term(String s, int a) {
		functor = s;
		arity = a;
		bound = true;
		deref = false;
		args = new Term[arity];
	}

	/** Binds a variable to a term */
	public final void bind(Term t) {
		if (this == t)
			return; // XXXX binding to self should have no effect
		if (!bound) {
			bound = true;
			deref = true;
			ref = t;
		} else
			SourceGetter.out.errorMsg("Term.bind(" + this + ")", "Can't bind nonvar!");
	}

	/** Unbinds a term -- ie. resets it to a variable */
	public final void unbind() {
		bound = false;
		ref = null;
		// XXXX Now possible for a bind to have had no effect so ignore safety
		// test
		// XXXX if (bound) bound = false;
		// XXXX else IO.error("Term.unbind","Can't unbind var!");
	}

	/**
	 * Used to set specific arguments. A primitive way of constructing terms is
	 * to create them with Term(s,f) and then build up the arguments. Using the
	 * parser is much simpler
	 */
	final public void setarg(int pos, Term val) {
		// only to be used on bound terms
		if (bound & (!deref))
			args[pos] = val;
		else
			SourceGetter.out.errorMsg("Term.setarg(" + pos + "," + val + ")",
					"Can't setarg on variables!");
	}

	/** Retrieves an argument of a term */
	public final Term getarg(int pos) {
		// should check if pos is valid
		if (bound) {
			if (deref) {
				return ref.getarg(pos);
			} else {
				return args[pos];
			}
		} else {
			SourceGetter.out.errorMsg("Term.getarg", "Error - lookup on unbound term!");
			return null; // dummy ... never reached
		}
	}

	/** Gets the functor of a term */
	public final String getfunctor() {
		if (bound) {
			if (deref) {
				return ref.getfunctor();
			} else
				return functor;
		} else
			return "";
	}

	/** Gets the arity of a term */
	public final int getarity() {
		if (bound) {
			if (deref) {
				return ref.getarity();
			} else
				return arity;
		} else
			return 0;
	}

	/** Checks whether a variable occurs in the term */
	// XXXX Since a variable is not considered to occur in itself
	// XXXX added occurs1 and a new front end called occurs.
	final boolean occurs(int var) {
		if (varid == var)
			return false;
		else
			return occurs1(var);
	}

	final boolean occurs1(int var) {
		if (bound) {
			if (deref)
				return ref.occurs1(var);
			else { // bound and not deref
				for (int i = 0; i < arity; i++)
					if (args[i].occurs1(var))
						return true;
				return false;
			}
		} else
			// unbound
			return (varid == var);
	}

	/**
	 * Unification is the basic primitive operation in logic programming.
	 * 
	 * @param s
	 *            - the stack is used to store the addresses of variables which
	 *            are bound by the unification. This is needed when
	 *            backtracking.
	 */
	final public boolean unify(Term t, Stack s) {
		if (bound & deref)
			return ref.unify(t, s);
		if (t.bound & t.deref)
			return unify(t.ref, s);
		if (bound & t.bound) { // bound and not deref
			if (functor.equals(t.getfunctor()) & (arity == t.getarity())) {
				for (int i = 0; i < arity; i++)
					if (!args[i].unify(t.getarg(i), s))
						return false;
				return true;

			} else
				return false; // functor/arity don't match ...

		} // at least one arg not bound ...
		if (bound) {
			// return t.unify(this,s);
			// XXXX Added missing occur check
			if (occurcheck) {
				if (this.occurs(t.varid))
					return false;
			} // XXXX
			t.bind(this);
			s.push(t);
			return true;
		}
		// Do occurcheck if turned on ...
		if (occurcheck) {
			if (t.occurs(varid))
				return false;
		}
		this.bind(t);
		s.push(this); // save for backtracking
		return true;
	}

	/**
	 * refresh creates new variables. If the variables allready exist in its
	 * argument then they are used - this is used when parsing a clause so that
	 * variables throught the clause are shared. Includes a copy operation
	 */
	public final Term refresh(Term l[]) {
		Term t;
		if (bound) {
			if (deref)
				return ref.refresh(l);
			else { // bound & not deref
				t = new Term(functor, arity);
				// t.bound = true; t.deref = false;
				// t.functor = functor; t.arity = arity;
				for (int i = 0; i < arity; i++)
					t.args[i] = args[i].refresh(l);
				return t;
			}
		} else
			// unbound
			return getvar(l, varid);
	}

	private final Term getvar(Term l[], int v) {
		if (l[v] == null)
			l[v] = new Term();
		return l[v];
	}

	/** Displays a term in standard notation */
	public final String toString() {
		String s;
		if (bound) {
			if (deref)
				return ref.toString();
			else {
				if (functor.equals("null") & arity == 0 & prettyprint)
					return "[]";
				if (functor.equals("cons") & arity == 2 & prettyprint) {
					Term t;
					s = "[" + args[0];
					t = args[1];

					while (t.getfunctor().equals("cons") & t.getarity() == 2) {
						s = s + "," + t.getarg(0);
						t = t.getarg(1);
					}

					if (t.getfunctor().equals("null") & t.getarity() == 0)
						s = s + "]";
					else
						s = s + "|" + t + "]";

					return s;
				} else {
					s = functor;
					if (arity > 0) {
						s = s + "(";
						for (int i = 0; i < (arity - 1); i++)
							s = s + args[i].toString() + ",";
						s = s + args[arity - 1].toString() + ")";
					}
				}
				return s;
			}
		} else
			return ("_" + varid);
	}

	/**
	 * This constructor is the simplest way to construct a term. The term is
	 * given in standard notation. Example
	 * <tt>Term(new ParseString("p(1,a(X,b))"))</tt>
	 * 
	 * @see ParseString
	 */
	public Term(ParseString ps) throws Exception {
		Term ts[];
		int i = 0;
		Term t;

		ts = new Term[300]; // arbitrary

		if (Character.isLowerCase(ps.current())
				| (internalparse & ps.current() == '_')) {
			functor = ps.getname();
			bound = true;
			deref = false;

			if (ps.current() == '(') {
				ps.advance();
				ps.skipspace();
				ts[i++] = new Term(ps);
				ps.skipspace();

				while (ps.current() == ',') {
					ps.advance();
					ps.skipspace();
					ts[i++] = new Term(ps);
					ps.skipspace();
				}

				if (ps.current() != ')')
					ps.parseerror("Expecting: ``)''");

				ps.advance();

				args = new Term[i];

				for (int j = 0; j < i; j++)
					args[j] = ts[j];

				arity = i;

			} else
				arity = 0;
		} else

		if (Character.isUpperCase(ps.current())) {
			bound = true;
			deref = true;
			ref = ps.getvar();
		} else

		if (Character.isDigit(ps.current())) {
			functor = ps.getnum();
			arity = 0;
			bound = true;
			deref = false;
		} else

		if (ps.current() == '[') {
			ps.advance();

			if (ps.current() == ']') {
				ps.advance();
				functor = "null";
				arity = 0;
				bound = true;
				deref = false;
			} else {
				ps.skipspace();
				ts[i++] = new Term(ps);
				ps.skipspace();

				while (ps.current() == ',') {
					ps.advance();
					ps.skipspace();
					ts[i++] = new Term(ps);
					ps.skipspace();
				}

				if (ps.current() == '|') {
					ps.advance();
					ps.skipspace();
					ts[i++] = new Term(ps);
					ps.skipspace();
				} else
					ts[i++] = new Term("null", 0);

				if (ps.current() != ']')
					ps.parseerror("Expecting ``]''");

				ps.advance();

				bound = true;
				deref = false;

				functor = "cons";
				arity = 2;
				args = new Term[2];

				for (int j = i - 2; j > 0; j--) {
					t = new Term("cons", 2);
					t.setarg(0, ts[j]);
					t.setarg(1, ts[j + 1]);
					ts[j] = t;
				}

				args[0] = ts[0];
				args[1] = ts[1];

			}
		} else
			ps.parseerror("Term should begin with a letter, a digit or ``[''");
	}

}
